slice
container.abstract_array.slice
Precondition
Inherited from Sequence.slice
pre debug : from ≥ 0 debug : to = 0 || (if is_array_backed || debug_level > 1 then is_valid_index to-1 else true) debug : from <= to
Postcondition
Inherited from Sequence.slice
post debug: result.finite.is_yes_or_unknown debug: result.count = (to-from).as_i32
Type Parameters
0.095dev (GIT hash fe578dbae82d257bfb6d755e3b05abbf37247dbe)
up to 'to' (excluded).
Complexity:
index access : O(1)
count : O(1)